Skip to content

Do not generate nil_exprt in bv_get #4197

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Apr 4, 2019
Merged

Do not generate nil_exprt in bv_get #4197

merged 1 commit into from
Apr 4, 2019

Conversation

tautschnig
Copy link
Collaborator

We have all the information available, and should thus always generate concrete
values.

This is an attempt to address what has been discussed in #4153, but completely missing automated tests (I've done some local hacks on my L1-renaming branch). @thk123 would you be able to take a look and possibly assist with tests?

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig mentioned this pull request Feb 15, 2019
Closed
7 tasks
kroening
kroening reviewed Feb 16, 2019
View reviewed changes
src/solvers/flattening/boolbv_get.cpp

std::size_t sub_width=boolbv_width(subtype);
const member_exprt member(expr, c.get_name(), subtype);
op.push_back(
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Doesn't this then produce a member of nil?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That was me being lazy, which I shouldn't have been. Now passing a proper index_exprt.

kroening
kroening reviewed Feb 16, 2019
View reviewed changes
src/solvers/flattening/boolbv_get.cpp
@@ -168,9 +168,11 @@ exprt boolbvt::bv_get_rec(

const typet &subtype = components[component_nr].type();

const member_exprt member(
expr, components[component_nr].get_name(), subtype);
return union_exprt(
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As above, the nil_exprt is now an index_exprt and there can't be a nil_exprt reaching this point.

kroening
kroening reviewed Feb 16, 2019
View reviewed changes
src/solvers/flattening/boolbv_get.cpp
@@ -262,14 +268,14 @@ exprt boolbvt::bv_get_rec(
}
}

return nil_exprt();
UNREACHABLE;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There should be a PRECONDITION in the if(...) above on the type, or a failure here will be hard to debug.

Copy link
Collaborator Author

@tautschnig tautschnig Mar 29, 2019 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have borrowed a bit from #2548. (Edit: sorry, that doesn't actually help here, I've added the appropriate PRECONDITION instead.)

@tautschnig tautschnig assigned tautschnig and unassigned thk123 Feb 27, 2019
@thk123 thk123 mentioned this pull request Mar 12, 2019
Merged
5 tasks
@tautschnig tautschnig changed the title Do not generate nil_exprt in bv_get Do not generate nil_exprt in bv_get [depends-on: #4372] Mar 30, 2019
@tautschnig tautschnig force-pushed the bv_get-unbounded-array branch from 45edfa9 to e9ffb73 Compare March 30, 2019 00:16
allredj
allredj reviewed Mar 30, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: e9ffb73).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106406254

@tautschnig tautschnig force-pushed the bv_get-unbounded-array branch from e9ffb73 to 14253f3 Compare March 30, 2019 09:18
allredj
allredj reviewed Mar 30, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 14253f3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106420870

martin-cs
martin-cs approved these changes Apr 1, 2019
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems like only the last commit is actually connected to the title of the PR.

@tautschnig
Copy link
Collaborator Author

It seems like only the last commit is actually connected to the title of the PR.

Ah, sorry, I should have said so: the first two are from #4372, which I've marked this one as dependent-on.

@tautschnig tautschnig force-pushed the bv_get-unbounded-array branch from 14253f3 to 7da0d6f Compare April 3, 2019 07:43
@tautschnig tautschnig changed the title Do not generate nil_exprt in bv_get [depends-on: #4372] Do not generate nil_exprt in bv_get Apr 3, 2019
allredj
allredj reviewed Apr 3, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 7da0d6f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106870338

@tautschnig tautschnig force-pushed the bv_get-unbounded-array branch 2 times, most recently from 2319ead to 69c8b0d Compare April 3, 2019 13:37
allredj
allredj reviewed Apr 3, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 69c8b0d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106929748

@tautschnig tautschnig added Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers and removed do not merge labels Apr 3, 2019
@tautschnig
Do not generate nil_exprt in bv_get
57874c4 
We have all the information available, and should thus always generate
concrete values.
@tautschnig tautschnig force-pushed the bv_get-unbounded-array branch from 69c8b0d to 57874c4 Compare April 3, 2019 16:09
@tautschnig tautschnig assigned thk123 and allredj and unassigned tautschnig Apr 3, 2019
allredj
allredj reviewed Apr 3, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 57874c4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106944413

@tautschnig tautschnig merged commit 79b1e09 into diffblue:develop Apr 4, 2019
@tautschnig tautschnig deleted the bv_get-unbounded-array branch April 4, 2019 17:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kroening kroening kroening left review comments

@allredj allredj allredj left review comments

@martin-cs martin-cs martin-cs approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@thk123 thk123

@allredj allredj

Labels
bugfix Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@tautschnig @kroening @martin-cs @allredj @thk123